$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$prop\{i:l\}), $L$:($T$ List), $x$:$T$.
\\[0ex](($\exists$$L_{1}$:$T$ List. (iseg($T$; $L_{1}$; append($L$; cons($x$; []))) $\wedge$ $P$($L_{1}$)))
\\[0ex]$\wedge$ ($\neg$($\exists$$L_{1}$:$T$ List. (iseg($T$; $L_{1}$; $L$) $\wedge$ $P$($L_{1}$)))))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($P$(append($L$; cons($x$; []))) $\wedge$ ($\neg$($\exists$$L_{1}$:$T$ List. (iseg($T$; $L_{1}$; $L$) $\wedge$ $P$($L_{1}$)))))